"A tweet saying 'Why revert back to natural language when there are formal methods using symbols?'
Public.icon
Speaking of which, although lightweight formal methods, including type systems, can prove sanity in the world of symbols, are specifications created by humans and written in natural language guaranteeing any sanity?
To everyone, are formal methods like Test-Driven Development concrete things?
In simple terms, can it be used as a DSL (domain-specific language) for requirements definition?
Why isn't it popular?
Isn't it agile development that doesn't write tests (formal methods(?)) to meet the minimum requirements?
It seems that there are several levels
Level 0
Perform a formal specification description and informally develop the program. It is called "lightweight formal methods." It is a choice that can quickly achieve cost-effectiveness.
Level 1
Develop and verify using formal methods and generate programs more formalistically. For example, perform detailed attribute proof from specification description. It is a suitable choice for high reliability systems.
Level 2
Completely demonstrate with automatic theorem proving. It costs money to prepare tools and requires time to describe the system rigorously. Don't do it unless it is worth it, given the loss due to errors (e.g. important parts of microprocessor design).
But it seems difficult to always do it properly tkgshn.icon*2Previous companies, interviews and appearances related to oneself.icon
In normal system design, you would write specifications in natural language and draw UML diagrams if necessary. https://gyazo.com/585ba2f66616fbe18c0514d2dee5f123 Model checking can analyze whether properties such as "Before making a payment, you can choose ramen unlimited times" and "An order without specified ramen will not occur" hold for this type of state transition system.
The selling point of formal methods is to reduce the cost of bug fixing by finding bugs during the design and implementation stages. This is based on the Waterfall development model where the "design" -> "implementation" -> "testing" stages are clearly separated.
However, in modern software development, Agile development models have become mainstream.
Huh, is that so?
Is this argument against "Testing is essential for agile development"?
Even with formal methods, bugs cannot be reduced to zero.
Well, that's true. tkgshn.icon*3
chatgpt.icon
Formal methods are techniques used in software design and development to express accurate specifications and designs using mathematical methods and formal languages, and to automatically analyze and verify them. Formal methods are an important technique, particularly for the development of advanced or mission-critical systems, as they can increase the accuracy, reliability, and safety of software.
Formal methods include formal specification languages, formal proofs, and model checking. Formal specification languages are used to express system specifications in mathematical form, which is difficult to express in natural or programming languages. Formal proof is to mathematically prove that the specification is satisfied. Model checking is a method for automatically generating a system model, and verifying the properties that the model must satisfy.
Formal methods are useful not only in fields that require accuracy, but also in programming and system development, allowing you to improve code quality and prevent bugs from entering the system by using formal methods.
[http://formal.mri.co.jp/outline/#:~:text=Formal%20Method%20is%20a%20method%20that%20provides%20a%20mechanism%20for%20logically%20reasoning%20about%20information%20systems%20(software,%20hardware,%20etc.)%20by%20describing%20requirements,%20design,%20etc.%20using%20a%20language%20called%20a%20"formal%20specification%20description%20language"%20that%20is%20mathematically%20rigorous.%20It%20is%20a%20generic%20term%20for%20many%20methods%20that%20differ%20depending%20on%20mathematical%20theories%20and%20other%20factors.%20There%20are%20over%20100%20different%20methods%20proposed,%20each%20with%20differences%20in%20the%20suitability%20of%20the%20scope%20of%20the%20object%20to%20be%20described%20and%20the%20verification%20purpose.%20Some%20of%20the%20formal%20methods%20that%20are%20relatively%20commonly%20used%20in%20practice%20include%20B%20Method,%20Event-B,%20VDM++,%20SPIN,%20NuSMV,%20and%20Z.%20Formal%20methods%20are%20increasingly%20being%20applied%20to%20real%20systems,%20especially%20safety-critical%20and%20mission-critical%20systems%20in%20the%20railway,%20aviation,%20finance,%20and%20security%20fields.%20 Is%20it%20a%20concept%20or%20tkgshn.icon*4%20? Formal%20methods%20are%20a%20generic%20term%20for%20many%20methods%20that%20differ%20depending%20on%20mathematical%20theories%20and%20other%20factors.%20There%20are%20over%20100%20different%20methods%20proposed,%20each%20with%20differences%20in%20the%20suitability%20of%20the%20scope%20of%20the%20object%20to%20be%20described%20and%20the%20verification%20purpose.%20Some%20of%20the%20formal%20methods%20that%20are%20relatively%20commonly%20used%20in%20practice%20include%20B%20Method,%20Event-B,%20VDM++,%20SPIN,%20NuSMV,%20and%20Z.%20Formal%20methods%20are%20increasingly%20being%20applied%20to%20real%20systems,%20especially%20safety-critical%20and%20mission-critical%20systems%20in%20the%20railway,%20aviation,%20finance,%20and%20security%20fields.%20
Wow,%20tkgshn.icon*3%20
https://gyazo.com/24a98cc886f7d1e8bbb8a764b76a157a
https://gyazo.com/61545c84a814cddedb3598b55443f15a
Hey,%20we%20should%20definitely%20use%20this.
https://gyazo.com/9085364fec511ac22d7f47b126036f61
Is%20there%20a%20sense%20of%20level%20or%20something%20like%20that?
There%20are%20two%20methods%20for%20creating%20reliable%20software:%20traditional%20"unit%20and%20integration%20testing"%20and%20"formal%20methods",%20which%20have%20been%20actively%20researched%20in%20recent%20years.%20Formal%20methods%20are%20a%20new%20method%20that%20efficiently%20inspects%20software%20by%20incorporating%20the%20ideas%20of%20mathematical%20logic,%20but%20it%20is%20not%20yet%20widely%20known.%20Here%20is%20an%20overview%20of%20these%20methods. %20
Unit%20and%20integration%20testing
In unit and integration testing, a large system is divided into smaller parts for inspection. In unit testing, a program (mock/stub) is combined with the divided small parts (unit) and appropriate input/output is given to observe the unit's behavior from both inside and outside, such as whether the unit's reaction is appropriate and whether the internal changes of the unit are appropriate.
https://gyazo.com/2d288f32effe58c6cb55d91f93d6a9fe
Formal methods
In contrast to unit and integration testing, formal methods abstract the system and test it. In formal methods, the design work is carried out in order of high-level abstraction (waterfall model). Instead of directly testing the code, formal methods verify the operation of high-level abstract systems and the connection between different levels of abstraction. This enables the detection of system defects at an early stage (even if coding has not been done yet), promotes the development of hierarchical system design, and improves the efficiency and maintainability of system development.
https://gyazo.com/97d8e27254acb31ea057e91b9b499009
4. Advantages and disadvantages of formal methods
Advantages:
Formal methods are a rigorous verification based on logic, with few test case omissions. In fact, many bugs that were overlooked in unit and integration testing have been discovered through the use of formal methods. The verification of abstracted systems has a high affinity with hierarchical software design, which leads to the improvement of software design. As a result, software maintainability and extensibility become easier. In addition, systematic verification can be carried out in the upstream stage, which improves the efficiency of software development.
Disadvantages:
To master the verification tools of (current) formal methods, the ability to read and write logical expressions is required, which can be a high hurdle for many people.
How to introduce formal methods?
Formal methods have such attractive advantages. Especially in the development of large-scale and distributed systems, their effects are significant. However, on the other hand, they also have shortcomings that need to be overcome. The best way to introduce formal methods at this stage is to entrust their introduction and in-house education to specialized institutions that are proficient in formal methods. In this process, design the application of formal methods that suits your company, arrange its operation method, and conduct in-house education at the same time. If you can complete this series of large routines, the subsequent application of formal methods should proceed smoothly.
The intended readers are those who are similar to me before learning - software engineers who have not received specialized education in computer science or mathematics and have relied mainly on practical work and self-study.
Awesometkgshn.icon*4
Formal methods can apparently discover problems more abstractly and comprehensively than testing.
I see, certainly according to the seven principles of testing, "tests can show the presence of defects, but not their absence." If formal methods can cover this weakness, they are amazing. However, I don't really understand the theory. If something is not written, can't it be found?
Completely agreetkgshn.icon*4
Some explanations say that formal methods are based on mathematical logic. I don't understand. Even in normal programming, I write if statements. What's different? Is it that it's formalized? I see... what is formalization anyway? The code of a program is for the machine to read, but isn't that formalization? What is the difference between normal programming and formal methods?
This is exactly the same and I laughed.
My initial question, "Isn't the code of a program also formalized?" is correct. The programming language used by programmers on a daily basis is a formal language. It is a language that specifies the available character set and grammar rules and does not allow ambiguous syntax.
To check the results, programmers have to enumerate specific cases in the unit tests they are familiar with. For example, when {a:3, b:4, c:5} holds, when {a:5, b:12, c:13} holds, and so on.
I see.
However, with proof, you can demonstrate that the theorem holds for any infinite right triangle, not just individual cases. In the proof of junior high school mathematics, we derived the theorem by transforming the already obvious definition through operations such as drawing auxiliary lines on the right triangle diagram.
Let's consider the Pythagorean theorem. It is a theorem that a2+b2=c2 holds in a right triangle consisting of two sides a and b and a hypotenuse of length c.
https://gyazo.com/8eae8788e91ec550adb1d43d820afd06
When we move away from the range of middle and high school mathematics, we can say the following. A proposition that can be considered correct unconditionally is called an axiom. By repeatedly applying inference rules to axioms, we can derive theorems. Proof is the process of organizing the logical structure of this.
ChatGPT.iconBoth formal methods and category theory aim to capture problems from a higher-dimensional perspective by using abstraction and mathematical thinking, so there is a certain relationship between them.
Formal methods are a method of designing or verifying systems using mathematical methods or formal expressions to improve the accuracy and reliability of software. In formal methods, high-dimensional mathematical concepts and expressions may be used to more accurately represent the system.
On the other hand, category theory is a branch of mathematics that abstracts and generalizes concepts and structures, allowing common theories and methods to be applied to different fields and problems. In category theory, objects and arrows are abstracted and their relationships are defined, allowing commonalities in various fields to be captured.
The way formal methods and category theory work is by looking at problems from a higher-dimensional perspective and generalizing them, aiming to construct theories and methods applicable to different fields and problems. In that sense, it can also be related to the idea of "thinking in higher dimensions" talked about in the quote "You might become even stronger in life if you learn a little more about arithmetic and mathematical concepts" tkgshn icon 6. However, defining this theorem is quite difficult, isn't it? previous companies, interviews and appearances related to oneself icon. Depending on the situation and requirements, it seems that sometimes the logical system should be changed. For example, if you want to verify that an algorithm satisfies the specifications, you would describe the pre- and post-conditions using Hoare logic. When checking the properties of a system with a long lifecycle, expressions using temporal logic such as "will eventually be true" or "will always be true" can also be used. It's a tradeoff between complexity and strong expression complexity and strong representation are tradeoffs, and what's important is the appropriate level of abstraction in the specification and modeling. Sometimes, domain-specific languages (DSL) that limit expression can be an effective solution DSL. Pretty useful in software development for large projects.
https://gyazo.com/bcff1333100a3a823f5b32bdce6bd21a
https://gyazo.com/f5b25987834fa3be3159b0256db7c2a2
https://gyazo.com/2eac28b6bb432a34c587df38fe665443
I see, tkgshn.icon*4
In the end, it is one of the concepts of DSL https://gyazo.com/840947782c18ccc3fc3c7113672d531f